(set-option :produce-unsat-cores true)
(declare-sort C)
(declare-const x C)
(declare-const y C)
(declare-const z C)
(declare-fun P (C C) Bool)
(declare-fun Q (C C) Bool)

; we assert the premise (and name it premise)
(assert (! (= y z) :named premise))
; we assert the negation of the conclusion
(assert (! (not (=> (and (Q z x) (P x z)) (and (P x y) (Q x y)))) :named conclusion))

(check-sat)
;(get-model)

; now we assert this quantified formula (for commutativity) to add an additional axiom to the theory
(assert (! (forall ((x C)) (forall ((y C)) (=> (Q x y) (Q y x)))) :named commutativity))

; this time it turns out to be valid (there exists no counterexample)
(check-sat)
; the unsat core tells us that all assertions are needed for the unsat (validity) result
;(get-unsat-core)